\begin{tabbing}
send\_onceR\=\{\$done:ut2, \$tg:ut2, \$b:ut2, \$done1:ut2\}\+
\\[0ex]($T$; $A$; $f$; $l$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\oplus$(\=[onceR\=\{\$b:ut2, \$done1:ut2\}\+\+
\\[0ex](source($l$))
\-\\[0ex]; \=sends locl("\$b")(v:Unit) on $l$:\+
\\[0ex]tagged([$\langle$"\$tg"$,\,$$\lambda$$s$,$v$. [$f$($s$("\$done"))]$\rangle$],State("\$done" : $A$),v):"\$tg" : $T$])
\-\-
\end{tabbing}